% Francesco Cotto
% SpPdP
% TypeChecker per picalcolo


%% Per gestire il type checker poliadico:
%% sfrutto il "pattern matching" del prolog.
%% solo dove serve aggiungo esplicitamente le regole per le liste...

/* Grammatica

se C e' una categoria sintattica allora C* e' una sequenza finita (eventualmente vuota) di
espressioni di categoria C (realizzata con una lista)

Var ::= a| b | c | x | y | z | Vari   (i in Nat)

Num ::= 0 | 1 | ...

Bool ::= true | false

Exp ::= Var | Num | Bool | Exp + Exp | Exp and Exp

Proc ::= stop | input(Var, Var*, Proc) | rec(Var, Var*, Proc)
      |  output(Var, Exp*, Proc) | par(Proc, Proc) | nu(Var, Proc)
      |  ite(Exp, Proc, Proc)

Type ::= int | bool | proc | chan(Type*)    

Typing ::= hasType(Var, Type)

Env ::= Typing*

*/


% Operatori (in ml solo and)

:- op(110,xfx,and).
:- op(110,xfx,or).
:- op(110,xfx,neq).

% Utilita:

%memberEnv(vartipo, env): vartipo appartiene all ambiente?
%questa regola serve per instanziare (singoletto) l ambiente =assioma=
memberEnv(X, [X1]) :- unify_with_occurs_check(X,X1), !.
memberEnv(X, [X1|_]) :- unify_with_occurs_check(X,X1), !.
memberEnv(X, [_|Y]) :- memberEnv(X,Y).


% cancella una sola occorrenza di X dalla lista
% in un contesto ben formato non posso avere piu' volte la stessa var...
deleteEnv([X|Rest], X, Rest) :- !.
deleteEnv([Y | Rest], X, [Y|Deleted]) :- deleteEnv(Rest, X, Deleted).

deleteEnvList(L,[],L) :- !.
deleteEnvList(LI,[DH|DT],LF) :- deleteEnv(LI,DH,NLF), deleteEnvList(NLF,DT,LF).

% Predicati relativi alle cat. sintatiche

isVar(X) :- atom(X), true\=X, false\=X.

%%   il caso isVar([]) e' compreso in atom([]) -> true
isVar([H|T]) :- isVar(H),!, isVar(T),!.

% Predicati relativi agli ambienti
%% in generale non ho bisogno di ridefinirli per il calcolo poliadico
%% in quanto queste regole non fanno assunzioni sul tipo della variabile

% inDom(Var, Delta) sse Var in dom(Delta)
% ossia la variabile e' gia' nell'ambiente a prescindere dal tipo...
inDom(Var, Delta) :- memberEnv(hasType(Var,_), Delta).

% typeInEnv(Var, Type, Delta) sse Delta(Var) = Type
% come inDom ma si controlla anche il tipo
typeInEnv(Var,T,Delta) :- memberEnv(hasType(Var,T),Delta).

% mergeEnv(Delta1, Delta2, Delta3) sse
% Delta3 = Delta1 unione Delta2 e' ambiente ben formato
% L'unione di due ambienti e' ancora un ambiente?
% Versione DeLiguoro:
% prima di tutto: fail merge se in delta2 c'e' gia' Var ma con T non unificabile

% per poliadico: nessuna modifica. Per liste unificazione su T in hasType
% viene preservato l ordine. ex. chan([int,bool]) neq chan([bool,int])

mergeEnv([hasType(Var, T)|_], Delta2, _) :-
        not(memberEnv(hasType(Var, T), Delta2)),
        inDom(Var, Delta2), !, mergeEnvFailMsg(Var,T,Delta2),fail.

mergeEnv([], Delta, Delta) :- !.

mergeEnv([hasType(Var,T)|Delta1], Delta2, Delta3) :-
        memberEnv(hasType(Var,T), Delta2), !,
        mergeEnv(Delta1, Delta2, Delta3), !.

mergeEnv([hasType(Var,T)|Delta1], Delta2, [hasType(Var,T)|Delta3]) :-
        mergeEnv(Delta1, Delta2, Delta3), !.

mergeEnvFailMsg(V,T1,D2):- 
        memberEnv(hasType(V,T2),D2),
        write('[mergeEnv] Fail per conflitto sul tipo della var: '),write(V),
        write(' con tipi: '),write(T1),
        write(' e: '),write(T2).
                          

%% ...
bindEnvVar([hasType(Var,T)], [Var],[T]) :- !.
bindEnvVar([hasType(VH,TH)|ET], [VH|VT],[TH|TT]) :- bindEnvVar(ET,VT,TT), !.
bindEnvVar(_, [], [_]).

bindEnvVar([hasType(Var,T)],Var,T).

% der(Delta, Term, Type) sse Delta |- Term:Type

% Assegnamento per le espressioni

% questi atomi non ammettono altre risoluzioni...

der(_, true, bool).

der(_, false, bool).

der(_, Num, int) :- integer(Num), !.

%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
der(_,[],[sync]) :- !.
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% la inseriamo qui per non fare riconoscere stop come una variabile
% inoltre usiamo il cut in quanto stop non e' "ulteriormente" risolubile...
% Nil e' derivabile con ogni ambiente (sempre vero)
der(_, stop, proc) :- !.


der([hasType(Var,T)], Var, T) :-
        isVar(Var).
      
der(Delta, Exp1 + Exp2, int) :-
        der(Delta1, Exp1, int),
        der(Delta2, Exp2, int),
        mergeEnv(Delta1,Delta2,Delta).
        
der(Delta, Exp1 and Exp2, bool) :-
        der(Delta1, Exp1, bool),
        der(Delta2, Exp2, bool),
        mergeEnv(Delta1,Delta2,Delta).
        
%% derivo il tipo di una lista di espressioni,
%% in questo modo posso tenere le stesse regole
%% di deriviazione per output e input

%% in particolare se delta(a) = t(a) delta([a]) = t([a])

%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
der(Delta, [E], [T]) :- der(Delta, E, T),!.

der(Delta, [EH|ET], [TEH|TET]) :-
           der(Delta, EH, TEH),
           der(Delta, ET, TET).
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% alla base di tutto questo esericizio c'e' il problema di trasformare
% una regola di inferenza logica in una rule del prolog, che ha invece
% un comportamento procedurale...
% Sulla questione vedere appunti DeLiguoro... e relativo uso di mergeEnv
der(Delta, par(P, Q), proc) :-
        der(Delta1, P, proc),
        der(Delta2, Q, proc),
        mergeEnv(Delta1, Delta2, Delta).

% La restriction (nu ch)P aggiunghe il canale ch in env di P       
der(Delta, nu(Ch, P), proc) :-
        der(DeltaP, P, proc),
        mergeEnv([hasType(Ch, chan(_))], DeltaP, DeltaTmp),
        deleteEnv(DeltaTmp, hasType(Ch,chan(_)), Delta).

% if then else
der(Delta, ite(Exp, Proc1, Proc2), proc) :-
        der(DeltaC, Exp, bool),
        der(Delta1, Proc1, proc),
        der(Delta2, Proc2, proc),
        mergeEnv(Delta1, Delta2, DeltaTmp),
        mergeEnv(DeltaTmp, DeltaC, Delta),!.

% pcalcolo monadico: input output rec
%% (per calcolo poliadico qui servono regole distinte...?
%%  2 strategie: cerco di estendere le regole esistenti al caso poliadico
%%               oppure aggiungo delle regole per il calcolo poliadico (X) )
%% soluzione: vedere derivazione di lista di espressioni

% Output non fa namebinding...
% verifichiamo solo che il processo sia "well formed" 
der(Delta, output(Ch, Out, P), proc) :-
        der(DeltaP, P, proc),
        der(DeltaParam, Out, T),!,
        mergeEnv([hasType(Ch, chan(T))], DeltaP, DeltaTmp),
        mergeEnv(DeltaTmp, DeltaParam, Delta).


% nb. input rende la var In bound in P
% ossia aggiunge In nel contesto di P
% ma il contesto del proc. input non ha la var In (quindi delete)
der(Delta, input(Ch, In, P), proc) :-
        % oss. serve una variabile e non un valore!
        % Spunto: introdurre prima le regole di fail (con relativo msg)
        % e poi scrivere regole senza questo tipo di controlli
        isVar(In),
        der(DeltaP, P, proc), !,
        bindEnvVar(DeltaBindVar, In, T),
        mergeEnv(DeltaBindVar, DeltaP, DeltaTmp), !,
        deleteEnvList([hasType(Ch, chan(T))|DeltaTmp], DeltaBindVar, Delta).
        

% se derivo P derivo anche *P, visto che in questa logica il contesto
% non si consuma come se fosse una risorsa limitata...
% quindi riscrivo il rec come semplice input
der(Delta, rec(Ch, In, P), proc) :- der(Delta, input(Ch,In,P), proc).

%% main print

printEnv([]) :- write('#\n'),!.

printEnv([hasType(Var, Type) | Tail ]) :-
         write(Var),write(':'),printType(Type),write(' '),
         printEnv(Tail),!.


printType(T) :- (atom(T) ; gensym(t, Ty), T = Ty), !,
                write(T).

printType([H]) :- printType(H),!.
printType([H|T]) :- printType(H),write(','), printType(T).

                
                
printType(chan(T)) :- write('^['), printType(T),!, write(']'),!.


tc(Term) :- der(Delta, Term, proc),
        printEnv(Delta).
        
% Test

test :- test_monadico, test_poliadico.

test_monadico :- tc(output(a,1,stop)),
        tc(input(a,b,stop)),
        tc(par(input(a,b,stop),output(a,1,stop))),
        tc(par(input(a,b,input(c,b,stop)),par(output(a,1,stop),output(a,1,stop)))),
        tc(par(input(a,b,output(a2,b,stop)),par(output(a,1,stop),output(a,1,stop)))),
        tc(par(input(c,a,ite(a,output(c, b, stop),output(c, b,stop))),output(c,true and b,stop))),
        tc(par(output(c,a,input(c,v,output(c,v+1,stop))),output(d,a,stop))),
        tc(output(c,a and true,output(d,b+1,stop))),
        tc(nu(c,output(c,a,output(c,a+1,stop)))),
        tc(par(nu(c,output(c,1,stop)),input(c,v,stop))),
        tc(nu(c,par(output(c,1,stop),input(c,v,stop)))),
        tc(input(a,a,output(a,1,stop))),
        tc(output(a,b,output(b,1,stop))),
        write(' end test monadico \n').

test_poliadico :-
        tc(par(output(a,[],stop),input(a,[],stop))),
        tc(par(nu(c,output(c,[1],stop)),input(c,[v],stop))),
	tc(par(input(a,[a1,a2,a3],stop),output(a,[1,2,3,true],stop))),
	write(' end test poliadico ').





